@inproceedings{abhashkumar2019tiramisu,
  title = {Tiramisu: {{Fast}} and {{General Network Verification}}},
  shorttitle = {Tiramisu},
  author = {Abhashkumar, Anubhavnidhi and Gember-Jacobson, Aaron and Akella, Aditya},
  date = {2019-06},
  eprint = {1906.02043},
  eprinttype = {arxiv},
  eprintclass = {Cs},
  url = {http://arxiv.org/abs/1906.02043},
  urldate = {2020-09-01},
  langid = {english},
  keywords = {Computer Science - Networking and Internet Architecture}
}

@inproceedings{abhashkumar2020tiramisu,
  title = {Tiramisu: Fast Multilayer Network Verification},
  shorttitle = {Tiramisu},
  booktitle = {Proceedings of the 17th {{Usenix Conference}} on {{Networked Systems Design}} and {{Implementation}}},
  author = {Abhashkumar, Anubhavnidhi and Gember-Jacobson, Aaron and Akella, Aditya},
  date = {2020-02-25},
  series = {{{NSDI}}'20},
  pages = {201--220},
  publisher = {{USENIX Association}},
  location = {{USA}},
  isbn = {978-1-939133-13-7}
}

@article{akers1978binary,
  title = {Binary {{Decision Diagrams}}},
  author = {{Akers}},
  date = {1978-06},
  journaltitle = {IEEE Transactions on Computers},
  shortjournal = {IEEE Trans. Comput.},
  volume = {C-27},
  number = {6},
  pages = {509--516},
  issn = {0018-9340},
  doi = {10.1109/TC.1978.1675141},
  url = {http://ieeexplore.ieee.org/document/1675141/},
  urldate = {2023-05-09}
}

@inproceedings{al-shaer2009network,
  title = {Network Configuration in a Box: Towards End-to-End Verification of Network Reachability and Security},
  shorttitle = {Network Configuration in a Box},
  booktitle = {2009 17th {{IEEE International Conference}} on {{Network Protocols}}},
  author = {Al-Shaer, Ehab and Marrero, Will and El-Atawy, Adel and ElBadawi, Khalid},
  date = {2009-10},
  pages = {123--132},
  publisher = {{IEEE}},
  location = {{Plainsboro, NJ, USA}},
  doi = {10.1109/ICNP.2009.5339690},
  url = {http://ieeexplore.ieee.org/document/5339690/},
  urldate = {2023-05-22},
  eventtitle = {2009 17th {{IEEE International Conference}} on {{Network Protocols}} ({{ICNP}})},
  isbn = {978-1-4244-4635-3}
}

@inproceedings{al-shaer2010flowchecker,
  title = {{{FlowChecker}}: Configuration Analysis and Verification of Federated Openflow Infrastructures},
  shorttitle = {{{FlowChecker}}},
  booktitle = {Proceedings of the 3rd {{ACM}} Workshop on {{Assurable}} and Usable Security Configuration - {{SafeConfig}} '10},
  author = {Al-Shaer, Ehab and Al-Haj, Saeed},
  date = {2010},
  pages = {37},
  publisher = {{ACM Press}},
  location = {{Chicago, Illinois, USA}},
  doi = {10.1145/1866898.1866905},
  url = {http://portal.acm.org/citation.cfm?doid=1866898.1866905},
  urldate = {2023-01-04},
  eventtitle = {The 3rd {{ACM}} Workshop},
  isbn = {978-1-4503-0093-3},
  langid = {english}
}

@online{aldin2019consistency,
  title = {Consistency Models in Distributed Systems: {{A}} Survey on Definitions, Disciplines, Challenges and Applications},
  shorttitle = {Consistency Models in Distributed Systems},
  author = {Aldin, Hesam Nejati Sharif and Deldari, Hossein and Moattar, Mohammad Hossein and Ghods, Mostafa Razavi},
  date = {2019-02-08},
  eprint = {1902.03305},
  eprinttype = {arxiv},
  eprintclass = {cs},
  url = {http://arxiv.org/abs/1902.03305},
  urldate = {2023-04-20},
  pubstate = {preprint},
  keywords = {{Computer Science - Distributed, Parallel, and Cluster Computing}}
}

@article{alur1994theory,
  title = {A Theory of Timed Automata},
  author = {Alur, Rajeev and Dill, David L.},
  date = {1994-04-25},
  journaltitle = {Theoretical Computer Science},
  shortjournal = {Theor. Comput. Sci.},
  volume = {126},
  number = {2},
  pages = {183--235},
  issn = {0304-3975},
  doi = {10.1016/0304-3975(94)90010-8},
  url = {https://doi.org/10.1016/0304-3975(94)90010-8},
  urldate = {2023-08-11}
}

@inproceedings{beckett2018control,
  title = {Control Plane Compression},
  booktitle = {Proceedings of the 2018 {{Conference}} of the {{ACM Special Interest Group}} on {{Data Communication}}},
  author = {Beckett, Ryan and Gupta, Aarti and Mahajan, Ratul and Walker, David},
  date = {2018-08-07},
  series = {{{SIGCOMM}} '18},
  pages = {476--489},
  publisher = {{Association for Computing Machinery}},
  location = {{New York, NY, USA}},
  doi = {10.1145/3230543.3230583},
  url = {https://dl.acm.org/doi/10.1145/3230543.3230583},
  urldate = {2023-08-13},
  isbn = {978-1-4503-5567-4},
  keywords = {network verification,stable routing problem}
}

@article{beckett2019abstract,
  title = {Abstract Interpretation of Distributed Network Control Planes},
  author = {Beckett, Ryan and Gupta, Aarti and Mahajan, Ratul and Walker, David},
  date = {2019-12-20},
  journaltitle = {Proceedings of the ACM on Programming Languages},
  shortjournal = {Proc. ACM Program. Lang.},
  volume = {4},
  pages = {42:1--42:27},
  doi = {10.1145/3371110},
  url = {https://dl.acm.org/doi/10.1145/3371110},
  urldate = {2023-08-14},
  issue = {POPL},
  keywords = {Abstract Interpretation,Distributed Routing Protocols,Network Control Plane,Network Reliability,Network Simulation,Network Verification,Router Configuration Verification}
}

@incollection{beyer2021pjbdd,
  title = {{{PJBDD}}: {{A BDD Library}} for {{Java}} and {{Multi-Threading}}},
  shorttitle = {{{PJBDD}}},
  booktitle = {Automated {{Technology}} for {{Verification}} and {{Analysis}}},
  author = {Beyer, Dirk and Friedberger, Karlheinz and Holzner, Stephan},
  editor = {Hou, Zhe and Ganesh, Vijay},
  date = {2021},
  volume = {12971},
  pages = {144--149},
  publisher = {{Springer International Publishing}},
  location = {{Cham}},
  doi = {10.1007/978-3-030-88885-5_10},
  url = {https://link.springer.com/10.1007/978-3-030-88885-5_10},
  urldate = {2023-05-13},
  isbn = {978-3-030-88884-8 978-3-030-88885-5},
  langid = {english}
}

@incollection{bjorner2016ddnf,
  title = {{{ddNF}}: {{An Efficient Data Structure}} for {{Header Spaces}}},
  shorttitle = {{{ddNF}}},
  booktitle = {Hardware and {{Software}}: {{Verification}} and {{Testing}}},
  author = {Bjørner, Nikolaj and Juniwal, Garvit and Mahajan, Ratul and Seshia, Sanjit A. and Varghese, George},
  editor = {Bloem, Roderick and Arbel, Eli},
  date = {2016},
  volume = {10028},
  pages = {49--64},
  publisher = {{Springer International Publishing}},
  location = {{Cham}},
  doi = {10.1007/978-3-319-49052-6_4},
  url = {http://link.springer.com/10.1007/978-3-319-49052-6_4},
  urldate = {2023-06-08},
  isbn = {978-3-319-49051-9 978-3-319-49052-6},
  langid = {english}
}

@article{bryant1986graphbased,
  title = {Graph-{{Based Algorithms}} for {{Boolean Function Manipulation}}},
  author = {{Bryant}},
  date = {1986-08},
  journaltitle = {IEEE Transactions on Computers},
  shortjournal = {IEEE Trans. Comput.},
  volume = {C-35},
  number = {8},
  pages = {677--691},
  issn = {0018-9340},
  doi = {10.1109/TC.1986.1676819},
  url = {http://ieeexplore.ieee.org/document/1676819/},
  urldate = {2023-05-10}
}

@inproceedings{canini2012nice,
  title = {A {{NICE}} Way to Test Openflow Applications},
  booktitle = {Proceedings of the 9th {{USENIX}} Conference on {{Networked Systems Design}} and {{Implementation}}},
  author = {Canini, Marco and Venzano, Daniele and Perešíni, Peter and Kostić, Dejan and Rexford, Jennifer},
  date = {2012-04-25},
  series = {{{NSDI}}'12},
  pages = {10},
  publisher = {{USENIX Association}},
  location = {{USA}}
}

@unpublished{capogrosso2023hermesbdd,
  title = {{{HermesBDD}}: {{A}} Multi-Core and Multi-Platform Binary Decision Diagram Package},
  author = {Capogrosso, Luigi and Geretti, Luca and Cristani, Marco and Fummi, Franco and Villa, Tiziano},
  date = {2023},
  eprint = {2305.00039},
  eprinttype = {arxiv}
}

@inproceedings{croft2015systematically,
  title = {Systematically Exploring the Behavior of Control Programs},
  booktitle = {Proceedings of the 2015 {{USENIX Conference}} on {{Usenix Annual Technical Conference}}},
  author = {Croft, Jason and Mahajan, Ratul and Caesar, Matthew and Musuvathi, Madan},
  date = {2015-07-08},
  series = {{{USENIX ATC}} '15},
  pages = {165--176},
  publisher = {{USENIX Association}},
  location = {{USA}},
  isbn = {978-1-931971-22-5}
}

@article{FangXingHuBo2023wangluoyanzhengyanjiuzongshu,
  title = {网络验证研究综述},
  author = {方星, 胡波, 黄伟庆, 马超},
  date = {2023},
  journaltitle = {软件学报},
  volume = {34},
  number = {1},
  pages = {351},
  publisher = {{科学出版社}},
  doi = {10.13328/j.cnki.jos.006510},
  pagetotal = {30.0000}
}

@inproceedings{fayaz2016efficient,
  title = {Efficient Network Reachability Analysis Using a Succinct Control Plane Representation},
  booktitle = {Proceedings of the 12th {{USENIX}} Conference on {{Operating Systems Design}} and {{Implementation}}},
  author = {Fayaz, Seyed K. and Sharma, Tushar and Fogel, Ari and Mahajan, Ratul and Millstein, Todd and Sekar, Vyas and Varghese, George},
  date = {2016-11-02},
  series = {{{OSDI}}'16},
  pages = {217--232},
  publisher = {{USENIX Association}},
  location = {{USA}},
  isbn = {978-1-931971-33-1}
}

@inproceedings{feamster2005detecting,
  title = {Detecting {{BGP}} Configuration Faults with Static Analysis},
  booktitle = {Proceedings of the 2nd Conference on {{Symposium}} on {{Networked Systems Design}} \& {{Implementation}} - {{Volume}} 2},
  author = {Feamster, Nick and Balakrishnan, Hari},
  date = {2005-05-02},
  series = {{{NSDI}}'05},
  pages = {43--56},
  publisher = {{USENIX Association}},
  location = {{USA}}
}

@inproceedings{fogel2015general,
  title = {A {{General Approach}} to {{Network Configuration Analysis}}},
  booktitle = {12th {{USENIX}} Symposium on Networked Systems Design and Implementation},
  author = {Fogel, Ari and Fung, Stanley and Pedrosa, Luis and Walraed-Sullivan, Meg and Govindan, Ramesh and Mahajan, Ratul and Millstein, Todd},
  date = {2015},
  series = {{{NSDI}} '15},
  pages = {469--483}
}

@inproceedings{gember-jacobson2016fast,
  title = {Fast {{Control Plane Analysis Using}} an {{Abstract Representation}}},
  booktitle = {Proceedings of the 2016 {{ACM SIGCOMM Conference}}},
  author = {Gember-Jacobson, Aaron and Viswanathan, Raajay and Akella, Aditya and Mahajan, Ratul},
  date = {2016-08-22},
  series = {{{SIGCOMM}} '16},
  pages = {300--313},
  publisher = {{Association for Computing Machinery}},
  location = {{New York, NY, USA}},
  doi = {10.1145/2934872.2934876},
  url = {https://dl.acm.org/doi/10.1145/2934872.2934876},
  urldate = {2023-08-10},
  isbn = {978-1-4503-4193-6},
  keywords = {abstract representation,control plane,Network verification}
}

@inproceedings{giannarakis2019efficient,
  title = {Efficient {{Verification}} of {{Network Fault Tolerance}} via {{Counterexample-Guided Refinement}}},
  booktitle = {Computer {{Aided Verification}}},
  author = {Giannarakis, Nick and Beckett, Ryan and Mahajan, Ratul and Walker, David},
  editor = {Dillig, Isil and Tasiran, Serdar},
  date = {2019},
  series = {Lecture {{Notes}} in {{Computer Science}}},
  pages = {305--323},
  publisher = {{Springer International Publishing}},
  location = {{Cham}},
  doi = {10.1007/978-3-030-25543-5_18},
  isbn = {978-3-030-25543-5},
  langid = {english}
}

@inproceedings{guo2022flash,
  title = {Flash: Fast, Consistent Data Plane Verification for Large-Scale Network Settings},
  shorttitle = {Flash},
  booktitle = {Proceedings of the {{ACM SIGCOMM}} 2022 {{Conference}}},
  author = {Guo, Dong and Chen, Shenshen and Gao, Kai and Xiang, Qiao and Zhang, Ying},
  date = {2022-08-22},
  pages = {314--335},
  publisher = {{ACM}},
  location = {{Amsterdam Netherlands}},
  doi = {10.1145/3544216.3544246},
  url = {https://dl.acm.org/doi/10.1145/3544216.3544246},
  urldate = {2023-04-17},
  eventtitle = {{{SIGCOMM}} '22: {{ACM SIGCOMM}} 2022 {{Conference}}},
  isbn = {978-1-4503-9420-8},
  langid = {english}
}

@inproceedings{hanauer2020fully,
  title = {Fully {{Dynamic Single-source Reachability}} in {{Practice}}: {{An Experimental Study}}},
  booktitle = {2020 Proceedings of the Twenty-Second Workshop on Algorithm Engineering and Experiments},
  author = {Hanauer, Kathrin and Henzinger, Monika and Schulz, Christian},
  date = {2020},
  volume = {ALENEX'20},
  pages = {106--119},
  publisher = {{SIAM}}
}

@book{hill1981introduction,
  title = {Introduction to {{Switching Theory}} and {{Logical Design}}},
  author = {Hill, Frederick J. and Peterson, Gerald R.},
  date = {1981-02},
  edition = {3rd},
  publisher = {{John Wiley \& Sons, Inc.}},
  location = {{USA}},
  isbn = {978-0-471-04273-0},
  pagetotal = {617}
}

@inproceedings{holterbach2017swift,
  title = {{{SWIFT}}: {{Predictive Fast Reroute}}},
  booktitle = {Proceedings of the {{Conference}} of the {{ACM Special Interest Group}} on {{Data Communication}}},
  author = {Holterbach, Thomas and Vissicchio, Stefano and Dainotti, Alberto and Vanbever, Laurent},
  date = {2017},
  series = {{{SIGCOMM}} '17},
  pages = {460--473},
  publisher = {{ACM}},
  location = {{New York, NY, USA}},
  url = {http://doi.acm.org/10.1145/3098822.3098856},
  keywords = {BGP,Convergence,Fast Reroute,Root Cause Analysis}
}

@inproceedings{horn2017deltanet,
  title = {Delta-Net: {{Real-time}} Network Verification Using Atoms},
  booktitle = {Proceedings of the 14th {{USENIX}} Conference on Networked Systems Design and Implementation},
  author = {Horn, Alex and Kheradmand, Ali and Prasad, Mukul R.},
  date = {2017},
  series = {{{NSDI}}'17},
  pages = {735--749},
  publisher = {{USENIX Association}},
  location = {{USA}},
  isbn = {978-1-931971-37-9}
}

@inproceedings{horn2019precise,
  title = {A {{Precise}} and {{Expressive Lattice-theoretical Framework}} for {{Efficient Network Verification}}},
  author = {Horn, Alex and Kheradmand, Ali and Prasad, Mukul},
  date = {2019-10-01},
  pages = {1--12},
  doi = {10.1109/ICNP.2019.8888144}
}

@inproceedings{huang2011datalog,
  title = {Datalog and Emerging Applications: An Interactive Tutorial},
  shorttitle = {Datalog and Emerging Applications},
  booktitle = {Proceedings of the 2011 {{ACM SIGMOD International Conference}} on {{Management}} of Data},
  author = {Huang, Shan Shan and Green, Todd Jeffrey and Loo, Boon Thau},
  date = {2011-06-12},
  series = {{{SIGMOD}} '11},
  pages = {1213--1216},
  publisher = {{Association for Computing Machinery}},
  location = {{New York, NY, USA}},
  doi = {10.1145/1989323.1989456},
  url = {https://doi.org/10.1145/1989323.1989456},
  urldate = {2023-08-10},
  isbn = {978-1-4503-0661-4},
  keywords = {data exchange,data integration,datalog,declarative networking,program analysis,recursive query processing}
}

@inproceedings{jayaraman2019validating,
  title = {Validating {{Datacenters}} at {{Scale}}},
  booktitle = {Proceedings of the {{ACM Special Interest Group}} on {{Data Communication}}},
  author = {Jayaraman, Karthick and Bjørner, Nikolaj and Padhye, Jitu and Agrawal, Amar and Bhargava, Ashish and Bissonnette, Paul-Andre C and Foster, Shane and Helwer, Andrew and Kasten, Mark and Lee, Ivan and Namdhari, Anup and Niaz, Haseeb and Parkhi, Aniruddha and Pinnamraju, Hanukumar and Power, Adrian and Raje, Neha Milind and Sharma, Parag},
  date = {2019-08},
  series = {{{SIGCOMM}}'19},
  pages = {200--213},
  publisher = {{ACM}},
  location = {{Beijing China}},
  langid = {english}
}

@inproceedings{kazemian2012header,
  title = {Header {{Space Analysis}}: {{Static Checking For Networks}}},
  booktitle = {Proceedings of the 9th {{USENIX Conference}} on {{Networked Systems Design}} and {{Implementation}}},
  author = {Kazemian, Peyman and Varghese, George and McKeown, Nick},
  date = {2012},
  series = {{{NSDI}}'12},
  location = {{USA}},
  langid = {english}
}

@inproceedings{kazemian2013real,
  title = {Real Time Network Policy Checking Using Header Space Analysis},
  booktitle = {10th {{USENIX}} Symposium on Networked Systems Design and Implementation},
  author = {Kazemian, Peyman and Chang, Michael and Zeng, Hongyi and Varghese, George and McKeown, Nick and Whyte, Scott},
  date = {2013-04},
  series = {{{NSDI}}'13},
  pages = {99--111},
  publisher = {{USENIX Association}},
  location = {{Lombard, IL}},
  url = {https://www.usenix.org/conference/nsdi13/technical-sessions/presentation/kazemian}
}

@inproceedings{khurshid2012veriflow,
  title = {Veriflow: Verifying Network-Wide Invariants in Real Time},
  shorttitle = {Veriflow},
  booktitle = {{{ACM SIGCOMM Computer Communication Review}}},
  author = {Khurshid, Ahmed and Zhou, Wenxuan and Caesar, Matthew and Godfrey, P. Brighten},
  date = {2012-09-24},
  volume = {42},
  pages = {467--472},
  doi = {10.1145/2377677.2377766},
  url = {https://dl.acm.org/doi/10.1145/2377677.2377766},
  urldate = {2023-01-04},
  langid = {english}
}

@article{lamport1978time,
  title = {Time, Clocks, and the Ordering of Events in a Distributed System},
  author = {Lamport, Leslie},
  date = {1978-07},
  journaltitle = {Communications of the ACM},
  shortjournal = {Commun. ACM},
  volume = {21},
  number = {7},
  pages = {558--565},
  issn = {0001-0782, 1557-7317},
  doi = {10.1145/359545.359563},
  url = {https://dl.acm.org/doi/10.1145/359545.359563},
  urldate = {2023-04-19},
  langid = {english}
}

@inproceedings{lantz2010network,
  title = {A {{Network}} in a {{Laptop}}: {{Rapid Prototyping}} for {{Software-defined Networks}}},
  booktitle = {Proceedings of the 9th {{ACM SIGCOMM Workshop}} on {{Hot Topics}} in {{Networks}}},
  author = {Lantz, Bob and Heller, Brandon and McKeown, Nick},
  date = {2010},
  series = {Hotnets-{{IX}}},
  publisher = {{Association for Computing Machinery}},
  location = {{Monterey, California}},
  keywords = {emulation,open-flow,rapid prototyping,software defined networking,virtualization}
}

@article{lewis1998elements,
  title = {Elements of the {{Theory}} of {{Computation}}},
  author = {Lewis, Harry R and Papadimitriou, Christos H},
  date = {1998},
  journaltitle = {ACM SIGACT News},
  volume = {29},
  number = {3},
  pages = {62--78}
}

@article{li2019survey,
  title = {A {{Survey}} on {{Network Verification}} and {{Testing With Formal Methods}}: {{Approaches}} and {{Challenges}}},
  shorttitle = {A {{Survey}} on {{Network Verification}} and {{Testing With Formal Methods}}},
  author = {Li, Yahui and Yin, Xia and Wang, Zhiliang and Yao, Jiangyuan and Shi, Xingang and Wu, Jianping and Zhang, Han and Wang, Qing},
  date = {2019-21},
  journaltitle = {IEEE Communications Surveys \& Tutorials},
  shortjournal = {IEEE Commun. Surv. Tutorials},
  volume = {21},
  number = {1},
  pages = {940--969},
  issn = {1553-877X, 2373-745X},
  doi = {10.1109/COMST.2018.2868050},
  url = {https://ieeexplore.ieee.org/document/8453007/},
  urldate = {2023-01-03},
  langid = {english},
  keywords = {Formal methods,Network reliability,Network testing,Network verification,Software-defined network}
}

@article{li2020assisting,
  title = {Assisting {{Reachability Verification}} of {{Network Configurations Updates}} with {{NUV}}},
  author = {Li, Yahui and Wang, Zhiliang and Yin, Xia and Shi, Xingang and Wu, Jianping and Fangdan, Ye and Yao, Jiangyuan and Zhang, Han},
  date = {2020-05-01},
  journaltitle = {Computer Networks},
  shortjournal = {Computer Networks},
  volume = {177},
  pages = {107326},
  doi = {10.1016/j.comnet.2020.107326}
}

@inproceedings{liu2017crystalnet,
  title = {{{CrystalNet}}: {{Faithfully Emulating Large Production Networks}}},
  shorttitle = {{{CrystalNet}}},
  booktitle = {Proceedings of the 26th {{Symposium}} on {{Operating Systems Principles}}},
  author = {Liu, Hongqiang Harry and Zhu, Yibo and Padhye, Jitu and Cao, Jiaxin and Tallapragada, Sri and Lopes, Nuno P. and Rybalchenko, Andrey and Lu, Guohan and Yuan, Lihua},
  date = {2017-10},
  series = {{{SOSP}}'17},
  pages = {599--613},
  publisher = {{ACM}},
  location = {{Shanghai China}},
  url = {https://dl.acm.org/doi/10.1145/3132747.3132759},
  urldate = {2021-09-14},
  langid = {english}
}

@inproceedings{lopes2015checking,
  title = {Checking Beliefs in Dynamic Networks},
  booktitle = {Proceedings of the 12th {{USENIX}} Conference on Networked Systems Design and Implementation},
  author = {Lopes, Nuno P. and Bjørner, Nikolaj and Godefroid, Patrice and Jayaraman, Karthick and Varghese, George},
  date = {2015},
  series = {{{NSDI}}'15},
  pages = {499--512},
  publisher = {{USENIX Association}},
  location = {{USA}},
  isbn = {978-1-931971-21-8},
  pagetotal = {14}
}

@incollection{lopes2019fast,
  title = {Fast {{BGP Simulation}} of {{Large Datacenters}}},
  booktitle = {Verification, {{Model Checking}}, and {{Abstract Interpretation}}},
  author = {Lopes, Nuno P. and Rybalchenko, Andrey},
  editor = {Enea, Constantin and Piskac, Ruzica},
  date = {2019},
  volume = {11388},
  pages = {386--408},
  publisher = {{Springer International Publishing}},
  location = {{Cham}},
  url = {http://link.springer.com/10.1007/978-3-030-11245-5_18},
  urldate = {2021-09-13},
  langid = {english}
}

@incollection{lovato2014threadsafe,
  title = {A {{Thread-Safe Library}} for {{Binary Decision Diagrams}}},
  booktitle = {Software {{Engineering}} and {{Formal Methods}}},
  author = {Lovato, Alberto and Macedonio, Damiano and Spoto, Fausto},
  editor = {Giannakopoulou, Dimitra and Salaün, Gwen},
  date = {2014},
  volume = {8702},
  pages = {35--49},
  publisher = {{Springer International Publishing}},
  location = {{Cham}},
  doi = {10.1007/978-3-319-10431-7_4},
  url = {http://link.springer.com/10.1007/978-3-319-10431-7_4},
  urldate = {2023-05-13},
  isbn = {978-3-319-10430-0 978-3-319-10431-7}
}

@article{mai2011debugging,
  title = {Debugging the Data Plane with Anteater},
  author = {Mai, Haohui and Khurshid, Ahmed and Agarwal, Rachit and Caesar, Matthew and Godfrey, P. Brighten and King, Samuel Talmadge},
  date = {2011-10-22},
  journaltitle = {ACM SIGCOMM Computer Communication Review},
  shortjournal = {SIGCOMM Comput. Commun. Rev.},
  volume = {41},
  number = {4},
  pages = {290--301},
  issn = {0146-4833},
  doi = {10.1145/2043164.2018470},
  url = {https://dl.acm.org/doi/10.1145/2043164.2018470},
  urldate = {2023-01-03},
  langid = {english}
}

@inproceedings{michael2002high,
  title = {High Performance Dynamic Lock-Free Hash Tables and List-Based Sets},
  booktitle = {Proceedings of the Fourteenth Annual {{ACM}} Symposium on {{Parallel}} Algorithms and Architectures},
  author = {Michael, Maged M.},
  date = {2002-08-10},
  pages = {73--82},
  publisher = {{ACM}},
  location = {{Winnipeg Manitoba Canada}},
  doi = {10.1145/564870.564881},
  url = {https://dl.acm.org/doi/10.1145/564870.564881},
  urldate = {2023-05-13},
  eventtitle = {{{SPAA02}}: {{Fourteenth ACM Symposium}} on {{Parallelism}} in {{Algorithms}} and {{Architectures}}},
  isbn = {978-1-58113-529-9},
  langid = {english}
}

@inproceedings{prabhu2017predicting,
  title = {Predicting {{Network Futures}} with {{Plankton}}},
  booktitle = {Proceedings of the {{First Asia-Pacific Workshop}} on {{Networking}}},
  author = {Prabhu, Santhosh and Kheradmand, Ali and Godfrey, Brighten and Caesar, Matthew},
  date = {2017-08-03},
  series = {{{APNet}}'17},
  pages = {92--98},
  publisher = {{Association for Computing Machinery}},
  location = {{New York, NY, USA}},
  doi = {10.1145/3106989.3106991},
  url = {https://doi.org/10.1145/3106989.3106991},
  urldate = {2023-08-13},
  isbn = {978-1-4503-5244-4},
  keywords = {Correctness,Network Troubleshooting}
}

@article{quoitin2005modeling,
  title = {Modeling the {{Routing}} of an {{Autonomous System}} with {{C-BGP}}},
  author = {Quoitin, B. and Uhlig, S.},
  date = {2005-11},
  journaltitle = {IEEE Network},
  volume = {19},
  number = {6},
  pages = {12--19},
  url = {http://ieeexplore.ieee.org/document/1541716/},
  urldate = {2021-12-27},
  langid = {english}
}

@article{shalev2006splitordered,
  title = {Split-Ordered Lists: {{Lock-free}} Extensible Hash Tables},
  shorttitle = {Split-Ordered Lists},
  author = {Shalev, Ori and Shavit, Nir},
  date = {2006-05},
  journaltitle = {Journal of the ACM},
  shortjournal = {J. ACM},
  volume = {53},
  number = {3},
  pages = {379--405},
  issn = {0004-5411, 1557-735X},
  doi = {10.1145/1147954.1147958},
  url = {https://dl.acm.org/doi/10.1145/1147954.1147958},
  urldate = {2023-05-13},
  langid = {english}
}

@article{shannon1949synthesis,
  title = {The Synthesis of Two-Terminal Switching Circuits},
  author = {family=Shannon, given=Claude. E., given-i={{Claude}}E},
  date = {1949},
  journaltitle = {The Bell System Technical Journal},
  volume = {28},
  number = {1},
  pages = {59--98},
  doi = {10.1002/j.1538-7305.1949.tb03624.x}
}

@inproceedings{singh2015jupiter,
  ids = {singh2015jupiterb},
  title = {Jupiter Rising: {{A Decade}} of {{Clos Topologies}} and {{Centralized Control}} in {{Google}}'s {{Datacenter Network}}},
  booktitle = {Proceedings of the 2015 {{ACM}} Conference on Special Interest Group on Data Communication},
  author = {Singh, Arjun and Ong, Joon and Agarwal, Amit and Anderson, Glen and Armistead, Ashby and Bannon, Roy and Boving, Seb and Desai, Gaurav and Felderman, Bob and Germano, Paulie and Kanagala, Anand and Provost, Jeff and Simmons, Jason and Tanda, Eiichi and Wanderer, Jim and Hölzle, Urs and Stuart, Stephen and Vahdat, Amin},
  date = {2015},
  series = {{{SIGCOMM}} '15},
  pages = {183--197},
  publisher = {{Association for Computing Machinery}},
  location = {{New York, NY, USA}},
  url = {https://doi.org/10.1145/2785956.2787508},
  keywords = {centralized control and management,clos topology,datacenter networks,merchant silicon}
}

@inproceedings{stoenescu2016symnet,
  title = {{{SymNet}}: {{Scalable}} Symbolic Execution for Modern Networks},
  shorttitle = {{{SymNet}}},
  booktitle = {Proceedings of the 2016 {{ACM SIGCOMM Conference}}},
  author = {Stoenescu, Radu and Popovici, Matei and Negreanu, Lorina and Raiciu, Costin},
  date = {2016-08-22},
  series = {{{SIGCOMM}} '16},
  pages = {314--327},
  publisher = {{Association for Computing Machinery}},
  location = {{New York, NY, USA}},
  doi = {10.1145/2934872.2934881},
  url = {https://dl.acm.org/doi/10.1145/2934872.2934881},
  urldate = {2023-08-13},
  isbn = {978-1-4503-4193-6},
  keywords = {Data plane verification,Symbolic execution friendly language,SymNet}
}

@article{tomvandijk2017sylvan,
  title = {Sylvan: Multi-Core Framework for Decision Diagrams},
  shorttitle = {Sylvan},
  author = {{Tom van Dijk} and {Jaco van de Pol}},
  date = {2017-11},
  journaltitle = {International Journal on Software Tools for Technology Transfer},
  shortjournal = {Int J Softw Tools Technol Transfer},
  volume = {19},
  number = {6},
  pages = {675--696},
  issn = {1433-2779, 1433-2787},
  doi = {10.1007/s10009-016-0433-2},
  url = {http://link.springer.com/10.1007/s10009-016-0433-2},
  urldate = {2023-05-10},
  langid = {english}
}

@inproceedings{wang2015practical,
  title = {Practical Network-Wide Packet Behavior Identification by {{AP}} Classifier},
  booktitle = {Proceedings of the 11th {{ACM Conference}} on {{Emerging Networking Experiments}} and {{Technologies}}},
  author = {Wang, Huazhe and Qian, Chen and Yu, Ye and Yang, Hongkun and Lam, Simon S.},
  date = {2015-12-01},
  series = {{{CoNEXT}} '15},
  pages = {1--13},
  publisher = {{Association for Computing Machinery}},
  location = {{New York, NY, USA}},
  doi = {10.1145/2716281.2836095},
  url = {https://dl.acm.org/doi/10.1145/2716281.2836095},
  urldate = {2023-08-13},
  isbn = {978-1-4503-3412-9},
  keywords = {network verification,packet behavior identification,software defined networking}
}

@inproceedings{xiang2022network,
  title = {Network Can Check Itself: Scaling Data Plane Checking via Distributed, on-Device Verification},
  shorttitle = {Network Can Check Itself},
  booktitle = {Proceedings of the 21st {{ACM Workshop}} on {{Hot Topics}} in {{Networks}}},
  author = {Xiang, Qiao and Wen, Ridi and Huang, Chenyang and Wang, Yuxin and Le, Franck},
  date = {2022-11-14},
  pages = {85--92},
  publisher = {{ACM}},
  location = {{Austin Texas}},
  doi = {10.1145/3563766.3564095},
  url = {https://dl.acm.org/doi/10.1145/3563766.3564095},
  urldate = {2023-06-08},
  eventtitle = {{{HotNets}} '22: {{The}} 21st {{ACM Workshop}} on {{Hot Topics}} in {{Networks}}},
  isbn = {978-1-4503-9899-2},
  langid = {english}
}

@inproceedings{xiang2023centralized,
  title = {Beyond a {{Centralized Verifier}}: {{Scaling Data Plane Checking}} via {{Distributed}}, {{On-Device Verification}}},
  shorttitle = {Beyond a {{Centralized Verifier}}},
  booktitle = {Proceedings of the {{ACM SIGCOMM}} 2023 {{Conference}}},
  author = {Xiang, Qiao and Huang, Chenyang and Wen, Ridi and Wang, Yuxin and Fan, Xiwen and Liu, Zaoxing and Kong, Linghe and Duan, Dennis and Le, Franck and Sun, Wei},
  date = {2023-09-10},
  pages = {152--166},
  publisher = {{ACM}},
  location = {{New York NY USA}},
  doi = {10.1145/3603269.3604843},
  url = {https://dl.acm.org/doi/10.1145/3603269.3604843},
  urldate = {2023-11-13},
  eventtitle = {{{ACM SIGCOMM}} '23: {{ACM SIGCOMM}} 2023 {{Conference}}},
  isbn = {9798400702365},
  langid = {english}
}

@inproceedings{yang1997parallel,
  title = {Parallel Breadth-First {{BDD}} Construction},
  booktitle = {Proceedings of the Sixth {{ACM SIGPLAN}} Symposium on {{Principles}} and Practice of Parallel Programming  - {{PPOPP}} '97},
  author = {Yang, Bwolen and O'Hallaron, David R.},
  date = {1997},
  pages = {145--156},
  publisher = {{ACM Press}},
  location = {{Las Vegas, Nevada, United States}},
  doi = {10.1145/263764.263784},
  url = {http://portal.acm.org/citation.cfm?doid=263764.263784},
  urldate = {2023-05-09},
  eventtitle = {The Sixth {{ACM SIGPLAN}} Symposium},
  isbn = {978-0-89791-906-7},
  langid = {english}
}

@article{yang2016realtime,
  title = {Real-{{Time Verification}} of {{Network Properties Using Atomic Predicates}}},
  author = {Yang, Hongkun and Lam, Simon S.},
  date = {2016-04},
  journaltitle = {IEEE/ACM Transactions on Networking},
  shortjournal = {IEEE/ACM Trans. Networking},
  volume = {24},
  number = {2},
  pages = {887--900},
  issn = {1063-6692, 1558-2566},
  doi = {10.1109/TNET.2015.2398197},
  url = {http://ieeexplore.ieee.org/document/7059250/},
  urldate = {2023-01-04},
  keywords = {Automated tools,formal methods,network management,network policies and properties,protocol verification,reachability computation}
}

@article{yang2017scalable,
  title = {Scalable Verification of Networks with Packet Transformers Using Atomic Predicates},
  author = {Yang, Hongkun and Lam, Simon S.},
  date = {2017},
  journaltitle = {IEEE/ACM Transactions on Networking},
  volume = {25},
  number = {5},
  pages = {2900--2915},
  doi = {10.1109/TNET.2017.2720172}
}

@inproceedings{ye2020accuracy,
  title = {Accuracy, {{Scalability}}, {{Coverage}}: {{A Practical Configuration Verifier}} on a {{Global WAN}}},
  shorttitle = {Accuracy, {{Scalability}}, {{Coverage}}},
  booktitle = {Proceedings of the {{Annual}} Conference of the {{ACM Special Interest Group}} on {{Data Communication}} on the Applications, Technologies, Architectures, and Protocols for Computer Communication},
  author = {Ye, Fangdan and Yu, Da and Zhai, Ennan and Liu, Hongqiang Harry and Tian, Bingchuan and Ye, Qiaobo and Wang, Chunsheng and Wu, Xin and Guo, Tianchen and Jin, Cheng and She, Duncheng and Ma, Qing and Cheng, Biao and Xu, Hui and Zhang, Ming and Wang, Zhiliang and Fonseca, Rodrigo},
  date = {2020-07-30},
  series = {{{SIGCOMM}} '20},
  pages = {599--614},
  publisher = {{Association for Computing Machinery}},
  location = {{New York, NY, USA}},
  doi = {10.1145/3387514.3406217},
  url = {https://doi.org/10.1145/3387514.3406217},
  urldate = {2023-08-13},
  isbn = {978-1-4503-7955-7},
  keywords = {Network Configurations,Network Verification,Reliability}
}

@inproceedings{zeng2014libra,
  title = {Libra: {{Divide}} and {{Conquer}} to {{Verify Forwarding Tables}} in {{Huge Networks}}},
  booktitle = {11th {{USENIX}} Symposium on Networked Systems Design and Implementation},
  author = {Zeng, Hongyi and Zhang, Shidong and Ye, Fei and Jeyakumar, Vimalkumar and Ju, Mickey and Liu, Junda and McKeown, Nick and Vahdat, Amin},
  date = {2014-04},
  series = {{{NSDI}}'14},
  pages = {87--99},
  publisher = {{USENIX Association}},
  location = {{Seattle, WA}},
  url = {https://www.usenix.org/conference/nsdi14/technical-sessions/presentation/zeng}
}

@incollection{zhang2013sat,
  title = {{{SAT Based Verification}} of {{Network Data Planes}}},
  booktitle = {Automated {{Technology}} for {{Verification}} and {{Analysis}}},
  author = {Zhang, Shuyuan and Malik, Sharad},
  editor = {Van Hung, Dang and Ogawa, Mizuhito},
  date = {2013},
  volume = {8172},
  pages = {496--505},
  publisher = {{Springer International Publishing}},
  location = {{Cham}},
  doi = {10.1007/978-3-319-02444-8_43},
  url = {http://link.springer.com/10.1007/978-3-319-02444-8_43},
  urldate = {2023-01-03},
  isbn = {978-3-319-02443-1 978-3-319-02444-8}
}

@inproceedings{zhang2020apkeep,
  title = {{{APKeep}}: {{Realtime}} Network Verification for Real Networks},
  booktitle = {Proceedings of the 17th Usenix Conference on Networked Systems Design and Implementation},
  author = {Zhang, Peng and Liu, Xu and Yang, Hongkun and Kang, Ning and Gu, Zhengchang and Li, Hao},
  date = {2020},
  series = {{{NSDI}}'20},
  pages = {241--256},
  publisher = {{USENIX Association}},
  location = {{USA}},
  isbn = {978-1-939133-13-7}
}

@inproceedings{zhang2020incremental,
  title = {Incremental {{Network Configuration Verification}}},
  booktitle = {Proceedings of the 19th {{ACM Workshop}} on {{Hot Topics}} in {{Networks}}},
  author = {Zhang, Peng and Huang, Yuhao and Gember-Jacobson, Aaron and Shi, Wenbo and Liu, Xu and Yang, Hongkun and Zuo, Zhiqiang},
  date = {2020-11-04},
  series = {{{HotNets}} '20},
  pages = {81--87},
  publisher = {{Association for Computing Machinery}},
  location = {{New York, NY, USA}},
  doi = {10.1145/3422604.3425936},
  url = {https://dl.acm.org/doi/10.1145/3422604.3425936},
  urldate = {2023-08-13},
  isbn = {978-1-4503-8145-1},
  keywords = {configuration changes,incremental verification,network verification}
}

@inproceedings{zhang2022differential,
  title = {Differential {{Network Analysis}}},
  booktitle = {19th {{USENIX}} Symposium on Networked Systems Design and Implementation},
  author = {Zhang, Peng and Gember-Jacobson, Aaron and Zuo, Yueshang and Huang, Yuhao and Liu, Xu and Li, Hao},
  date = {2022-04},
  series = {{{NSDI}}'22},
  pages = {601--615},
  publisher = {{USENIX Association}},
  location = {{Renton, WA}},
  url = {https://www.usenix.org/conference/nsdi22/presentation/zhang-peng}
}

@inproceedings{zhang2022symbolic,
  title = {Symbolic Router Execution},
  booktitle = {Proceedings of the {{ACM SIGCOMM}} 2022 {{Conference}}},
  author = {Zhang, Peng and Wang, Dan and Gember-Jacobson, Aaron},
  date = {2022-08-22},
  pages = {336--349},
  publisher = {{ACM}},
  location = {{Amsterdam Netherlands}},
  doi = {10.1145/3544216.3544264},
  url = {https://dl.acm.org/doi/10.1145/3544216.3544264},
  urldate = {2023-01-04},
  eventtitle = {{{SIGCOMM}} '22: {{ACM SIGCOMM}} 2022 {{Conference}}},
  isbn = {978-1-4503-9420-8},
  langid = {english}
}

@inproceedings{zhouautomatically,
  title = {Automatically {{Correcting Networks}} with {{NEAt}}},
  author = {Zhou, Wenxuan and Croft, Jason and Liu, Bingzhe and Ang, Elaine and Caesar, Matthew},
  url = {https://www.usenix.org/conference/nsdi18/presentation/zhou},
  urldate = {2020-10-12},
  isbn = {978-1-939133-01-4}
}
